Problem:
a__zeros() -> cons(0(),zeros())
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(0()) -> 0()
a__zeros() -> zeros()
a__tail(X) -> tail(X)
Proof:
Complexity Transformation Processor:
strict:
a__zeros() -> cons(0(),zeros())
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(0()) -> 0()
a__zeros() -> zeros()
a__tail(X) -> tail(X)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tail](x0) = x0,
[mark](x0) = x0 + 44,
[a__tail](x0) = x0 + 5,
[cons](x0, x1) = x0 + x1 + 1,
[zeros] = 0,
[0] = 0,
[a__zeros] = 0
orientation:
a__zeros() = 0 >= 1 = cons(0(),zeros())
a__tail(cons(X,XS)) = X + XS + 6 >= XS + 44 = mark(XS)
mark(zeros()) = 44 >= 0 = a__zeros()
mark(tail(X)) = X + 44 >= X + 49 = a__tail(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 45 >= X1 + X2 + 45 = cons(mark(X1),X2)
mark(0()) = 44 >= 0 = 0()
a__zeros() = 0 >= 0 = zeros()
a__tail(X) = X + 5 >= X = tail(X)
problem:
strict:
a__zeros() -> cons(0(),zeros())
a__tail(cons(X,XS)) -> mark(XS)
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
a__zeros() -> zeros()
weak:
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tail](x0) = x0 + 10,
[mark](x0) = x0,
[a__tail](x0) = x0 + 10,
[cons](x0, x1) = x0 + x1 + 28,
[zeros] = 106,
[0] = 85,
[a__zeros] = 106
orientation:
a__zeros() = 106 >= 219 = cons(0(),zeros())
a__tail(cons(X,XS)) = X + XS + 38 >= XS = mark(XS)
mark(tail(X)) = X + 10 >= X + 10 = a__tail(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 28 >= X1 + X2 + 28 = cons(mark(X1),X2)
a__zeros() = 106 >= 106 = zeros()
mark(zeros()) = 106 >= 106 = a__zeros()
mark(0()) = 85 >= 85 = 0()
a__tail(X) = X + 10 >= X + 10 = tail(X)
problem:
strict:
a__zeros() -> cons(0(),zeros())
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
a__zeros() -> zeros()
weak:
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tail](x0) = x0,
[mark](x0) = x0 + 1,
[a__tail](x0) = x0,
[cons](x0, x1) = x0 + x1 + 1,
[zeros] = 32,
[0] = 8,
[a__zeros] = 33
orientation:
a__zeros() = 33 >= 41 = cons(0(),zeros())
mark(tail(X)) = X + 1 >= X + 1 = a__tail(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 2 >= X1 + X2 + 2 = cons(mark(X1),X2)
a__zeros() = 33 >= 32 = zeros()
a__tail(cons(X,XS)) = X + XS + 1 >= XS + 1 = mark(XS)
mark(zeros()) = 33 >= 33 = a__zeros()
mark(0()) = 9 >= 8 = 0()
a__tail(X) = X >= X = tail(X)
problem:
strict:
a__zeros() -> cons(0(),zeros())
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
weak:
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tail](x0) = x0 + 2,
[mark](x0) = x0 + 1,
[a__tail](x0) = x0 + 2,
[cons](x0, x1) = x0 + x1,
[zeros] = 0,
[0] = 0,
[a__zeros] = 1
orientation:
a__zeros() = 1 >= 0 = cons(0(),zeros())
mark(tail(X)) = X + 3 >= X + 3 = a__tail(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = cons(mark(X1),X2)
a__zeros() = 1 >= 0 = zeros()
a__tail(cons(X,XS)) = X + XS + 2 >= XS + 1 = mark(XS)
mark(zeros()) = 1 >= 1 = a__zeros()
mark(0()) = 1 >= 0 = 0()
a__tail(X) = X + 2 >= X + 2 = tail(X)
problem:
strict:
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
weak:
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Splitting Processor:
strict:
mark(tail(X)) -> a__tail(mark(X))
weak:
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {7,6,5}
transitions:
a__tail1(9) -> 10*
mark1(25) -> 31*
mark1(17) -> 10*
mark1(2) -> 10*
mark1(24) -> 25*
mark1(4) -> 10*
mark1(16) -> 17*
mark1(1) -> 10*
mark1(28) -> 10*
mark1(18) -> 19*
mark1(8) -> 9*
mark1(3) -> 10*
cons1(19,2) -> 9*
cons1(9,2) -> 9*
cons1(19,4) -> 9*
cons1(9,4) -> 9*
cons1(25,1) -> 9*
cons1(25,3) -> 9*
cons1(10,1) -> 10*
cons1(10,3) -> 10*
cons1(29,28) -> 6*
cons1(25,17) -> 7*
cons1(10,17) -> 10*
cons1(31,28) -> 10*
cons1(9,1) -> 9*
cons1(9,3) -> 9*
cons1(25,2) -> 9*
cons1(25,4) -> 9*
cons1(10,2) -> 10*
cons1(10,4) -> 10*
cons1(25,28) -> 17,5
cons1(17,2) -> 9*
cons1(17,4) -> 9*
tail1(9) -> 10*
01() -> 31,10,25,29
a__zeros1() -> 10,17
zeros1() -> 10,17,28
mark0(2) -> 7,5
mark0(4) -> 7,5
mark0(1) -> 7,5
mark0(3) -> 7,5
tail0(2) -> 7,1
tail0(4) -> 7,1
tail0(1) -> 7,1
tail0(3) -> 7,1
a__tail0(2) -> 7*
a__tail0(4) -> 7*
a__tail0(1) -> 7*
a__tail0(3) -> 7*
a__zeros0() -> 7,5,6
cons0(3,1) -> 2*
cons0(3,3) -> 2*
cons0(4,2) -> 2*
cons0(4,4) -> 2*
cons0(5,1) -> 7,5
cons0(5,3) -> 7,5
cons0(1,2) -> 2*
cons0(1,4) -> 2*
cons0(2,1) -> 2*
cons0(2,3) -> 2*
cons0(3,2) -> 2*
cons0(3,4) -> 2*
cons0(4,1) -> 2*
cons0(4,3) -> 2*
cons0(5,2) -> 7,5
cons0(5,4) -> 7,5
cons0(1,1) -> 2*
cons0(1,3) -> 2*
cons0(2,2) -> 2*
cons0(2,4) -> 2*
00() -> 7,5,3
zeros0() -> 7,5,6,4
1 -> 18*
2 -> 8*
3 -> 24*
4 -> 16*
10 -> 7,19,5
17 -> 9*
19 -> 9*
25 -> 9*
problem:
strict:
weak:
mark(tail(X)) -> a__tail(mark(X))
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
Qed
strict:
mark(cons(X1,X2)) -> cons(mark(X1),X2)
weak:
mark(tail(X)) -> a__tail(mark(X))
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 0 1 1]
[0 0 1 1]
[0 0 1 1]
[0 0 0 0]
interpretation:
[1 0 0 0] [0]
[0 0 0 0] [0]
[tail](x0) = [0 0 1 1]x0 + [0]
[0 0 0 0] [1],
[1 0 1 1] [0]
[0 0 1 1] [1]
[mark](x0) = [0 0 1 1]x0 + [1]
[0 0 0 0] [1],
[1 0 0 0] [1]
[0 0 1 0] [1]
[a__tail](x0) = [0 0 1 1]x0 + [0]
[0 0 0 0] [1],
[1 0 0 0] [1 0 1 1] [0]
[0 0 1 1] [0 0 1 0] [0]
[cons](x0, x1) = [0 0 1 1]x0 + [0 0 1 1]x1 + [0]
[0 0 0 0] [0 0 0 0] [1],
[0]
[0]
[zeros] = [1]
[0],
[0]
[0]
[0] = [0]
[0],
[1]
[1]
[a__zeros] = [1]
[1]
orientation:
[1 0 1 1] [1 0 2 2] [1] [1 0 1 1] [1 0 1 1] [0]
[0 0 1 1] [0 0 1 1] [2] [0 0 1 1] [0 0 1 0] [2]
mark(cons(X1,X2)) = [0 0 1 1]X1 + [0 0 1 1]X2 + [2] >= [0 0 1 1]X1 + [0 0 1 1]X2 + [2] = cons(mark(X1),X2)
[0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [1]
[1 0 1 1] [1] [1 0 1 1] [1]
[0 0 1 1] [2] [0 0 1 1] [2]
mark(tail(X)) = [0 0 1 1]X + [2] >= [0 0 1 1]X + [2] = a__tail(mark(X))
[0 0 0 0] [1] [0 0 0 0] [1]
[1] [1]
[1] [1]
a__zeros() = [1] >= [1] = cons(0(),zeros())
[1] [1]
[1] [0]
[1] [0]
a__zeros() = [1] >= [1] = zeros()
[1] [0]
[1 0 0 0] [1 0 1 1] [1] [1 0 1 1] [0]
[0 0 1 1] [0 0 1 1] [1] [0 0 1 1] [1]
a__tail(cons(X,XS)) = [0 0 1 1]X + [0 0 1 1]XS + [1] >= [0 0 1 1]XS + [1] = mark(XS)
[0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [1]
[1] [1]
[2] [1]
mark(zeros()) = [2] >= [1] = a__zeros()
[1] [1]
[0] [0]
[1] [0]
mark(0()) = [1] >= [0] = 0()
[1] [0]
[1 0 0 0] [1] [1 0 0 0] [0]
[0 0 1 0] [1] [0 0 0 0] [0]
a__tail(X) = [0 0 1 1]X + [0] >= [0 0 1 1]X + [0] = tail(X)
[0 0 0 0] [1] [0 0 0 0] [1]
problem:
strict:
weak:
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(tail(X)) -> a__tail(mark(X))
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Qed